The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

p(s(N)) → N
+(N, 0) → N
+(s(N), s(M)) → s(s(+(N, M)))
*(N, 0) → 0
*(s(N), s(M)) → s(+(N, +(M, *(N, M))))
gt(0, M) → False
gt(NzN, 0) → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0) → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0, N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0)
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0
gcd(0, N) → 0
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
+(s(N), s(M)) →⁺ s(s(+(N, M)))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0].
The pumping substitution is [N / s(N), M / s(M)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
+', *', gt, d, quot, gcd

They will be analysed ascendingly in the following order:
+' < *'
gt < quot
gt < gcd
d < quot
d < gcd

(8) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

The following defined symbols remain to be analysed:
+', *', gt, d, quot, gcd

They will be analysed ascendingly in the following order:
+' < *'
gt < quot
gt < gcd
d < quot
d < gcd

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

Induction Base:
+'(gen_s:0'3_0(0), gen_s:0'3_0(0)) →_R^Ω(1)
gen_s:0'3_0(0)

Induction Step:
+'(gen_s:0'3_0(+(n5_0, 1)), gen_s:0'3_0(+(n5_0, 1))) →_R^Ω(1)
s(s(+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)))) →_IH
s(s(gen_s:0'3_0(*(2, c6_0))))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(10) Complex Obligation (BEST)

(11) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

The following defined symbols remain to be analysed:
*', gt, d, quot, gcd

They will be analysed ascendingly in the following order:
gt < quot
gt < gcd
d < quot
d < gcd

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
*'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0))) → *4_0, rt ∈ Ω(n537₀)

Induction Base:
*'(gen_s:0'3_0(+(1, 0)), gen_s:0'3_0(+(1, 0)))

Induction Step:
*'(gen_s:0'3_0(+(1, +(n537_0, 1))), gen_s:0'3_0(+(1, +(n537_0, 1)))) →_R^Ω(1)
s(+'(gen_s:0'3_0(+(1, n537_0)), +'(gen_s:0'3_0(+(1, n537_0)), *'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0)))))) →_IH
s(+'(gen_s:0'3_0(+(1, n537_0)), +'(gen_s:0'3_0(+(1, n537_0)), *4_0)))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(13) Complex Obligation (BEST)

(14) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0))) → *4_0, rt ∈ Ω(n537₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

The following defined symbols remain to be analysed:
gt, d, quot, gcd

They will be analysed ascendingly in the following order:
gt < quot
gt < gcd
d < quot
d < gcd

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
gt(gen_s:0'3_0(n35359_0), gen_s:0'3_0(n35359_0)) → False, rt ∈ Ω(1 + n35359₀)

Induction Base:
gt(gen_s:0'3_0(0), gen_s:0'3_0(0)) →_R^Ω(1)
False

Induction Step:
gt(gen_s:0'3_0(+(n35359_0, 1)), gen_s:0'3_0(+(n35359_0, 1))) →_R^Ω(1)
gt(gen_s:0'3_0(n35359_0), gen_s:0'3_0(n35359_0)) →_IH
False

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(16) Complex Obligation (BEST)

(17) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0))) → *4_0, rt ∈ Ω(n537₀)
gt(gen_s:0'3_0(n35359_0), gen_s:0'3_0(n35359_0)) → False, rt ∈ Ω(1 + n35359₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

The following defined symbols remain to be analysed:
d, quot, gcd

They will be analysed ascendingly in the following order:
d < quot
d < gcd

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
d(gen_s:0'3_0(n35748_0), gen_s:0'3_0(n35748_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n35748₀)

Induction Base:
d(gen_s:0'3_0(0), gen_s:0'3_0(0)) →_R^Ω(1)
gen_s:0'3_0(0)

Induction Step:
d(gen_s:0'3_0(+(n35748_0, 1)), gen_s:0'3_0(+(n35748_0, 1))) →_R^Ω(1)
d(gen_s:0'3_0(n35748_0), gen_s:0'3_0(n35748_0)) →_IH
gen_s:0'3_0(0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(19) Complex Obligation (BEST)

(20) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0))) → *4_0, rt ∈ Ω(n537₀)
gt(gen_s:0'3_0(n35359_0), gen_s:0'3_0(n35359_0)) → False, rt ∈ Ω(1 + n35359₀)
d(gen_s:0'3_0(n35748_0), gen_s:0'3_0(n35748_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n35748₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

The following defined symbols remain to be analysed:
quot, gcd

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol quot.

(22) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0))) → *4_0, rt ∈ Ω(n537₀)
gt(gen_s:0'3_0(n35359_0), gen_s:0'3_0(n35359_0)) → False, rt ∈ Ω(1 + n35359₀)
d(gen_s:0'3_0(n35748_0), gen_s:0'3_0(n35748_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n35748₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

The following defined symbols remain to be analysed:
gcd

(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol gcd.

(24) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0))) → *4_0, rt ∈ Ω(n537₀)
gt(gen_s:0'3_0(n35359_0), gen_s:0'3_0(n35359_0)) → False, rt ∈ Ω(1 + n35359₀)
d(gen_s:0'3_0(n35748_0), gen_s:0'3_0(n35748_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n35748₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

No more defined symbols left to analyse.

(25) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(26) BOUNDS(n^1, INF)

(27) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0))) → *4_0, rt ∈ Ω(n537₀)
gt(gen_s:0'3_0(n35359_0), gen_s:0'3_0(n35359_0)) → False, rt ∈ Ω(1 + n35359₀)
d(gen_s:0'3_0(n35748_0), gen_s:0'3_0(n35748_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n35748₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

No more defined symbols left to analyse.

(28) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(29) BOUNDS(n^1, INF)

(30) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0))) → *4_0, rt ∈ Ω(n537₀)
gt(gen_s:0'3_0(n35359_0), gen_s:0'3_0(n35359_0)) → False, rt ∈ Ω(1 + n35359₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

No more defined symbols left to analyse.

(31) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(32) BOUNDS(n^1, INF)

(33) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n537_0)), gen_s:0'3_0(+(1, n537_0))) → *4_0, rt ∈ Ω(n537₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

No more defined symbols left to analyse.

(34) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(35) BOUNDS(n^1, INF)

(36) Obligation:

TRS:
Rules:
p(s(N)) → N
+'(N, 0') → N
+'(s(N), s(M)) → s(s(+'(N, M)))
*'(N, 0') → 0'
*'(s(N), s(M)) → s(+'(N, +'(M, *'(N, M))))
gt(0', M) → False
gt(NzN, 0') → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0') → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0', N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0')
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0'
gcd(0', N) → 0'
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Types:
p :: s:0' → s:0'
s :: s:0' → s:0'
+' :: s:0' → s:0' → s:0'
0' :: s:0'
*' :: s:0' → s:0' → s:0'
gt :: s:0' → s:0' → False:True
False :: False:True
u_4 :: False:True → False:True
is_NzNat :: s:0' → False:True
True :: False:True
lt :: s:0' → s:0' → False:True
d :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
u_11 :: False:True → s:0' → s:0' → s:0'
u_1 :: False:True → s:0' → s:0' → s:0'
u_01 :: False:True → s:0'
u_21 :: False:True → s:0' → s:0' → s:0'
u_2 :: False:True → s:0'
gcd :: s:0' → s:0' → s:0'
u_02 :: False:True → s:0' → s:0'
u_31 :: False:True → False:True → s:0' → s:0' → s:0'
u_3 :: False:True → s:0' → s:0' → s:0'
hole_s:0'1_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(x))

No more defined symbols left to analyse.

(37) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(38) BOUNDS(n^1, INF)